\begin{tabbing}
fifo(${\it es}$;${\it codes}$;${\it decodes}$;$C$;$S$;$R$;$T$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:$C$.\+
\\[0ex]$\exists$\=$f$:\{$e$:es{-}E(${\it es}$)$\mid$ $R$($i$,$e$)\} $\rightarrow$\{$e$:es{-}E(${\it es}$)$\mid$ $\exists$$j$:$C$. ($S$($j$,$i$,$e$))\} \+
\\[0ex](antecedent{-}surjection(${\it es}$;$\lambda$$e$.$R$($i$,$e$);$\lambda$$e$.$\exists$$j$:$C$. ($S$($j$,$i$,$e$));$f$)
\\[0ex]\& (\=$\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $R$($i$,$e$)\} , $j$:\{$j$:$C$$\mid$ $S$($j$,$i$,$f$($e$))\} .\+
\\[0ex]${\it decodes}$($i$,$e$,es{-}state{-}when(${\it es}$;$e$)) = ${\it codes}$($j$,$i$,$f$($e$),es{-}state{-}when(${\it es}$;$f$($e$))) $\in$ $T$)
\-\\[0ex]\& (\=$\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $R$($i$,$e$)\} , ${\it e'}$:\{$e$:es{-}E(${\it es}$)$\mid$ $R$($i$,$e$)\} , $j$:$C$.\+
\\[0ex]($S$($j$,$i$,$f$($e$)))
\\[0ex]$\Rightarrow$ ($S$($j$,$i$,$f$(${\it e'}$)))
\\[0ex]$\Rightarrow$ es{-}causle(${\it es}$;$f$($e$);$f$(${\it e'}$))
\\[0ex]$\Rightarrow$ es{-}causle(${\it es}$;$e$;${\it e'}$)))
\-\-\-
\end{tabbing}